\begin{tabbing}
$\forall$\=${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $k$:Knd, $x$:Id, $n$:$\mathbb{N}$,\+
\\[0ex]$f$:(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow$${\it ds}$($x$)?Void).
\-\\[0ex]update{-}spec1($k$;$x$;$n$;$s$,$v$.$f$($s$,$v$)) $\in$ update{-}spec(${\it ds}$;${\it da}$)
\end{tabbing}